FDL - Nuprl Lemma : read-w-state-when

Nuprl Lemma : read-w-state-when

w:World.
FairFifo

(

e:E. (

x.state_when(e)(x,0)) = (

x.s(loc(e);time(e)).x(0))

x:Id

vartype(loc(e);x))

Definitions Id, t T, , x:AB(x), x:A. B(x), #$n, time(e), loc(e), s(i;t).x, f(a), x.A(x), vartype(i;x), s = t, , , s ~ t, {T}, P Q, SQType(T), World, FairFifo, E, <a, b>

Lemmas w-E wf, fair-fifo wf, world wf, w-state-when, rationals wf, w-vartype wf, w-s wf, w-loc wf, w-time wf, int inc rationals, Id wf